#ifdef KITSCHY_DEBUG_MEMORY 
#include "debug_memorymanager.h"
#endif

#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "stdarg.h"
#include "assert.h"

#include "BList.h"

#include "symbol.h"
#include "sort.h"
#include "ontology.h"
#include "featureterm.h"
#include "FTKBase.h"

#include "SpecialTerm.h"

#include "AWEntity.h"

//Auxiliar class and function definitions:
class SubsumptionStackNode {
public:
	SubsumptionStackNode(FeatureTerm *f1,FeatureTerm *f2,int state,
						 int feature_pos,
						 int *assignment,FeatureTerm **set1,int set1l,FeatureTerm **set2,int set2l,int assignment_pos) {
		m_f1=f1;
		m_f2=f2;
		m_state=state;
		m_feature_pos=feature_pos;
		
		m_assignment=assignment;
		m_set1=set1;
		m_set2=set2;
		m_set1l=set1l;
		m_set2l=set2l;
		m_assignment_pos=assignment_pos;
/*
		if (set1l>0) {
			if (set1l==1 && f1->isSet() && f1->set_values_quick()->Length()!=set1l) assert(false);			
			if (set1l>1 && !f1->isSet()) assert(false);
			if (set1l>1 && f1->isSet() && f1->set_values_quick()->Length()!=set1l) assert(false);			
			if (set2l==1 && f2->isSet() && f2->set_values_quick()->Length()!=set2l) assert(false);			
			if (set2l>1 && !f2->isSet()) assert(false);
			if (set2l>1 && f2->isSet() && f2->set_values_quick()->Length()!=set2l) assert(false);			
		} // if
*/
	} /* SubsumptionStackNode */ 

	FeatureTerm *m_f1;
	FeatureTerm *m_f2;
	int m_state;
	int m_feature_pos;

	int *m_assignment;
	FeatureTerm **m_set1,**m_set2;
	int m_set1l,m_set2l;
	int m_assignment_pos;
};

class SubsumptionBackTrackNode {
public:
	~SubsumptionBackTrackNode() {		
		if (m_node!=0) {
			delete []m_node->m_assignment;			
			delete []m_node->m_set1;
			delete []m_node->m_set2;
			delete m_node;
			m_node=0;
		} /* if */ 
		if (m_stack!=0) {
			SubsumptionStackNode *n;
			while(!m_stack->EmptyP()) {
				n=m_stack->ExtractIni();
				if (n->m_assignment!=0) {
					delete []n->m_assignment;
					delete []n->m_set1;
					delete []n->m_set2;
				} //* if */ 
				delete n;						
			} /* while */ 
			delete m_stack;
			m_stack=0;
		} /* if */ 

	} /* ~SubsumptionBackTrackNode */ 

	int n_bindings;
	List<SubsumptionStackNode> *m_stack;
	SubsumptionStackNode *m_node;
};


bool get_set_assignment(int l1,int l2,int *assignment,int failure_position);



bool FeatureTerm::subsumes(FeatureTerm *f)
{
	List<FeatureTermContainer> bindings_a;
	List<FeatureTermContainer> bindings_b;
	List<SubsumptionStackNode> stack;
	SubsumptionStackNode *stack_node;
	List<SubsumptionBackTrackNode> stack_backtracking;
	FeatureTerm *f1=0,*f2=0;
	FeatureTerm **set1=0,**set2=0;
	int set1l=0,set2l=0;
	int *assignment=0;
	int feature_pos=0;
	int assignment_pos=0;
	int state;	/*	0 - normal, 
					1 - already known to be false, 
					2 - already known to be true, 
					3 - continuing a previous started subsumption, so no initial tests needed */ 
	bool res=true;
	int i;

	if (m_ft==f->m_ft) return true;
	if (m_ft==0 || f->m_ft==0) return false;


//	printf("*---- Begin Subsumption ----*\n");
/*
	{
		char *s;
		s=toStringNOOS(0);
		printf("Pattern: %s\n",s);
		delete []s;
		s=f->toStringNOOS(0);
		printf("Object: %s\n",s);
		delete []s;
	}
*/

	stack.Insert(new SubsumptionStackNode(this,f,0, -1, 0,0,0,0,0,-1));
	{
		while(!stack.EmptyP()) {
			stack_node=stack.ExtractIni();
			f1=stack_node->m_f1;
			f2=stack_node->m_f2;
			state=stack_node->m_state;
			feature_pos=stack_node->m_feature_pos;
			assignment=stack_node->m_assignment;
			set1=stack_node->m_set1;
			set2=stack_node->m_set2;
			set1l=stack_node->m_set1l;
			set2l=stack_node->m_set2l;
			assignment_pos=stack_node->m_assignment_pos;
			delete stack_node;


			// Initial subsumption tests: name,sort, etc.
/*
			printf("Subsumption: (state = %i) (%i remaining) (%i backtrack points)\n",state, stack.Length(), stack_backtracking.Length());
			{
				char *s;
				s=f1->toStringNOOS();
				printf("f1: %s\n",s);
				delete []s;
				s=f2->toStringNOOS();
				printf("f2: %s\n",s);
				delete []s;
			}
*/
			if (state==0) {
				/* Test for path equalties: */ 
				if (f1->m_ft->m_data_type==f2->m_ft->m_data_type) {
					int pos;

					pos=bindings_a.PositionRef(f1->m_ft);
					if (pos!=-1) {
						if (bindings_b[pos]==f2->m_ft) {
							/* already known to be true: */ 
							state=2;
						} else {
							FeatureTermContainer *ftc=bindings_b[pos];
							switch(f1->m_ft->m_data_type) {
							case 0: if (f2->hasValue() &&
										ftc->m_data_type==0 &&
										f2->m_ft->m_value.m_i.m_value==ftc->m_value.m_i.m_value &&
										f2->m_ft->m_value.m_i.m_type==ftc->m_value.m_i.m_type) {
										state=2;
									} else {
										state=1;
									} /* if */ 
									break;
							default:
									state=1;
							} /* switch */ 
						} /* if */ 
					} /* if */ 
				} /* if */ 
//				printf("path test completed...\n");
			} /* if */ 

			if (state==0) {
				/* Test names: */ 
				if (f1->m_ft->m_name!=0) {
					if (f2->m_ft->m_name==0) {
						if (f2->m_ft->m_data_type!=4) {
							state=1;
						} /* if */ 
					} else {
						if (f2->m_ft->m_name->cmp(f1->m_ft->m_name)) state=2;
														        else state=1;
					} /* if */ 
				} /* if */ 
//				printf("name test completed...\n");
			} /* if */ 
	
			if (state==0) {
				/* Test sorts: */ 
				if (f1->m_ft->m_data_type!=5 &&
					f1->m_ft->m_data_type!=4 && f2->m_ft->m_data_type!=4 &&
					f1->getSort()!=0 && f2->getSort()!=0 &&
					!f1->getSort()->isSubsort(f2->getSort())) state=1;
//				printf("sort test completed...\n");
			} /* if */ 

			if (state==0 || state==2) {
				if (f1->m_ft->m_data_type==f2->m_ft->m_data_type) {
					bindings_a.Insert(f1->m_ft);
					bindings_b.Insert(f2->m_ft);
				} /* if */ 
			} /* if */ 

			if (state==3) state=0;

			// Subsumption:
			if (state==0) {			

				if (f1->m_ft->m_data_type==4 || f2->m_ft->m_data_type==4) {
					bool interrupted=false;

//					printf("Set subsumption...\n");

					// Prepare the sets:
					if (set1==0 || set2==0) {
						if (f1->m_ft->m_data_type==4) {
							if (f1->m_ft->m_value.m_set->Length()>0) {
								set1=new FeatureTerm *[f1->m_ft->m_value.m_set->Length()];
							} else {
								set1=0;
							} // if
							set1l=0;
							List<FeatureTerm> l;
							FeatureTerm *ft;

							l.Instance(*(f1->m_ft->m_value.m_set));
							l.Rewind();
							while(l.Iterate(ft)) set1[set1l++]=ft;
						} else {
							set1=new FeatureTerm *[1];
							set1l=0;
							set1[set1l++]=f1;
						} // if  
						if (f2->m_ft->m_data_type==4) {
							if (f2->m_ft->m_value.m_set->Length()>0) {
								set2=new FeatureTerm *[f2->m_ft->m_value.m_set->Length()];
							} else {
								set2=0;
							} // if
							set2l=0;
							List<FeatureTerm> l;
							FeatureTerm *ft;

							l.Instance(*(f2->m_ft->m_value.m_set));
							l.Rewind();
							while(l.Iterate(ft)) set2[set2l++]=ft;
						} else {
							set2=new FeatureTerm *[1];
							set2l=0;
							set2[set2l++]=f2;
						} // if  

//						printf("Set1: %i\nSet2: %i\n",set1l,set2l);

						if (set1l==0 || set1l>set2l) {
							if (set1l==0) state=2;
									 else state=1;
							set1l=0;
							set2l=0;
							if (set1!=0) delete []set1;
							if (set2!=0) delete []set2;
							set1=0;
							set2=0;
						} // if  

//					} else {
//						printf("Sets were already prepared: Set1: %i\nSet2: %i\n",set1l,set2l);
					} // if  

					// Assign an element of the set2 to each element of the set1:  
					if (state==0) {

						if (assignment==0) {
							assignment=new int[set1l];
							for(i=0;i<set1l;i++) assignment[i]=i;
							assignment_pos=0;	
/*							
							printf("..: [%p,%p] ",f1,f2);
							printf("{%i,%i} ",set1l,set2l);
							for(i=0;i<set1l;i++) printf("%i ",assignment[i]);
							printf("\n");
*/
						} // if 
/*
						if (assignment_pos==0) {
							printf("Set assignement: ");
							for(i=0;i<set1l;i++) {
								printf("%i ",assignment[i]);
							} // for  
							printf("\n");
						} // if  

						printf("Now checking position %i\n",assignment_pos);
*/
						if (assignment_pos>=set1l) {
							state=2;
						} else {

							// create a backtracking node:
//							printf("Backtrack node created at set position: %i\n",assignment_pos);
							{
								SubsumptionBackTrackNode *b_node;
								SubsumptionStackNode *s_node;
								List<SubsumptionStackNode> l;

								b_node=new SubsumptionBackTrackNode();
								b_node->n_bindings=bindings_a.Length();
								{
                                    int idx;
									int *assignment_copy=new int[set1l];
									FeatureTerm **set1_copy,**set2_copy;
									for(i=0;i<set1l;i++) assignment_copy[i]=assignment[i];
									set1_copy=new FeatureTerm *[set1l];
									for(idx=0;idx<set1l;idx++) set1_copy[idx]=set1[idx];
									set2_copy=new FeatureTerm *[set2l];
									for(idx=0;idx<set2l;idx++) set2_copy[idx]=set2[idx];
									b_node->m_node=new SubsumptionStackNode(f1,f2,3, -1, assignment_copy,set1_copy,set1l,set2_copy,set2l,assignment_pos);
								}
								b_node->m_stack=new List<SubsumptionStackNode>;
								l.Instance(stack);
								while(l.Iterate(s_node)) {
									if (s_node->m_assignment!=0) {
                                        int idx;
										int *assignment_copy=new int[s_node->m_set1l];
										FeatureTerm **set1_copy,**set2_copy;
										for(i=0;i<s_node->m_set1l;i++) assignment_copy[i]=s_node->m_assignment[i];
										set1_copy=new FeatureTerm *[s_node->m_set1l];
										for(idx=0;idx<s_node->m_set1l;idx++) set1_copy[idx]=s_node->m_set1[idx];
										set2_copy=new FeatureTerm *[s_node->m_set2l];
										for(idx=0;idx<s_node->m_set2l;idx++) set2_copy[idx]=s_node->m_set2[idx];

										b_node->m_stack->Add(new SubsumptionStackNode(s_node->m_f1,s_node->m_f2,s_node->m_state,
																					  s_node->m_feature_pos,
																					  assignment_copy,set1_copy,s_node->m_set1l,set2_copy,s_node->m_set2l,s_node->m_assignment_pos));
									} else {
										b_node->m_stack->Add(new SubsumptionStackNode(s_node->m_f1,s_node->m_f2,s_node->m_state,
																					  s_node->m_feature_pos,
																					  0,0,0,0,0,-1));
									} /* if */ 
								} /* while */ 

								stack_backtracking.Insert(b_node);
							}

							stack.Insert(new SubsumptionStackNode(f1,f2,3, -1, assignment,set1,set1l,set2,set2l,assignment_pos+1));
							stack.Insert(new SubsumptionStackNode(set1[assignment_pos],set2[assignment[assignment_pos]],0, -1, 0,0,0,0,0,-1));
							interrupted=true;
						} /* if */ 

						if (!interrupted) delete []assignment;
					} // if  
					
					if (!interrupted) {
						if (set1!=0) delete []set1;
						if (set2!=0) delete []set2;
						set1=0;
						set2=0;
						set1l=0;
						set2l=0;
					} // if
				} else {
					// Single object subsumption: 
//					printf("Single object subsumption...\n");
					if (!f1->hasValue()) {
						if (!f1->getSort()->isSubsort(f2->getSort())) state=1;
					} else {
						switch(f1->m_ft->m_data_type) {
						case DATATYPE_ABSTRACT:
								break;
						case DATATYPE_INTEGER: 
								{
									switch(f1->m_ft->m_value.m_i.m_type) {
									case -1:/* undefined */ 							
											if (f2->m_ft->m_data_type!=0) state=1;
											break;
									case 0: /* specific value: */ 
											if (f2->m_ft->m_data_type!=0 ||
												f2->m_ft->m_value.m_i.m_type!=0 ||
												f2->m_ft->m_value.m_i.m_value!=f1->m_ft->m_value.m_i.m_value) state=1;
											break;
									} /* switch */ 
								}
								break;
						case DATATYPE_FLOAT: /* Note: floats are considered more general than integers */ 
								{
									float f_value=0;
									int f_type=0;

									if (f2->m_ft->m_data_type==0) {
										f_value=(float)f2->m_ft->m_value.m_i.m_value;
										f_type=f2->m_ft->m_value.m_i.m_type;
									} /* if */ 
									if (f2->m_ft->m_data_type==1) {
										f_value=f2->m_ft->m_value.m_f.m_value;
										f_type=f2->m_ft->m_value.m_f.m_type;
									} /* if */ 

									if (f2->m_ft->m_data_type!=0 && f2->m_ft->m_data_type!=1) state=1;

									switch(f1->m_ft->m_value.m_f.m_type) {
									case -1:/* undefined */ 
											break;
									case 0: /* specific value: */ 
											if (f_type==-1 ||
												f_value!=f1->m_ft->m_value.m_f.m_value) state=1;
											break;
									} /* switch */ 
								} 
								break;
						case DATATYPE_SYMBOL: 
								if (f1->m_ft->m_value.m_s!=0) {
									if (f2->m_ft->m_value.m_s==0) {
										state=1;
									} else {
										if (f2->m_ft->m_data_type!=2) {
											state=1;
										} else {
											if (!f2->m_ft->m_value.m_s->cmp(f1->m_ft->m_value.m_s)) state=1;
										} /* if */ 
									} /* if */ 
								} /* if */ 
								break;
						case DATATYPE_FEATURETERM: 
//								printf("FeatureTerm Subsumption (current feature %i):\n",feature_pos);
								{
									List<Symbol> fnl;
									Symbol *fn;
									List<FeatureTerm> fvl;
									FeatureTerm *fv,*fv2;
									bool interrupted=false;

									fnl.Instance(*(f1->m_ft->m_value.m_ft.m_feature_name));
									fvl.Instance(*(f1->m_ft->m_value.m_ft.m_feature_value));
									fnl.GoTo(feature_pos+1);
									fvl.GoTo(feature_pos+1);
									feature_pos++;
									while(!interrupted && state==0 && fnl.Iterate(fn) && fvl.Iterate(fv)) {
										fv2=f2->featureValueQuick(fn);
										if (fv2==0) {
											state=1;
										} /* if */ 
										if (state!=1) {
											stack.Insert(new SubsumptionStackNode(f1,f2,3,feature_pos, 0,0,0,0,0,-1));
											stack.Insert(new SubsumptionStackNode(fv,fv2,0,-1, 0,0,0,0,0,-1));
											interrupted=true;
										} /* if */
										feature_pos++;
									} // while 
									if (!interrupted && state==0) state=2;
								}
								break;
						case DATATYPE_SPECIAL:
								if (!f1->m_ft->m_value.m_special->subsumes(f2)) state=1;
								break;
						} /* switch */ 
					} // if 

				} /* if */ 

			} /* if */ 

			if (state==1) {
//				printf("Fail\n");

				if (!stack_backtracking.EmptyP()) {
					// backtracking:
					SubsumptionBackTrackNode *b_node;
					SubsumptionStackNode *s_node;
					bool found=false;

//					printf("Backtracking... (%i nodes)\n",stack_backtracking.Length());

					do{
						b_node=stack_backtracking.ExtractIni();
						s_node=b_node->m_node;
//						printf("bt: [%p,%p] ",s_node->m_f1,s_node->m_f2);
						if (get_set_assignment(s_node->m_set1l,s_node->m_set2l,s_node->m_assignment,s_node->m_assignment_pos)) found=true;

						if (!found) delete b_node;
					}while(!found && !stack_backtracking.EmptyP());

					if (found) {
						// Reconstruct the stack and bindings:
						// stack:
						List<SubsumptionStackNode> l;						
						while(!stack.EmptyP()) {
							s_node=stack.ExtractIni();
							if (s_node->m_assignment!=0) {
								delete []s_node->m_assignment;

								s_node->m_set1l=0;
								s_node->m_set2l=0;
								delete []s_node->m_set1;
								delete []s_node->m_set2;
							} //  if  
							delete s_node;
						} /* while */ 
						l.Instance(*(b_node->m_stack));
						while(l.Iterate(s_node)) {
							if (s_node->m_assignment!=0) {
                                int idx;
								int *assignment_copy=new int[s_node->m_set1l];
								FeatureTerm **set1_copy,**set2_copy;
								for(i=0;i<s_node->m_set1l;i++) assignment_copy[i]=s_node->m_assignment[i];
								set1_copy=new FeatureTerm *[s_node->m_set1l];
								for(idx=0;idx<s_node->m_set1l;idx++) set1_copy[idx]=s_node->m_set1[idx];
								set2_copy=new FeatureTerm *[s_node->m_set2l];
								for(idx=0;idx<s_node->m_set2l;idx++) set2_copy[idx]=s_node->m_set2[idx];

								stack.Add(new SubsumptionStackNode(s_node->m_f1,s_node->m_f2,s_node->m_state,
																   s_node->m_feature_pos,
																   assignment_copy,set1_copy,s_node->m_set1l,set2_copy,s_node->m_set2l,s_node->m_assignment_pos));
							} else {
								stack.Add(new SubsumptionStackNode(s_node->m_f1,s_node->m_f2,s_node->m_state,
																   s_node->m_feature_pos,
																   0,0,0,0,0,-1));
							} /* if */ 
						} // while  
						if (b_node->m_node->m_assignment!=0) {
                            int idx;
							int *assignment_copy=new int[b_node->m_node->m_set1l];
							FeatureTerm **set1_copy,**set2_copy;
							for(i=0;i<b_node->m_node->m_set1l;i++) assignment_copy[i]=b_node->m_node->m_assignment[i];

							set1_copy=new FeatureTerm *[b_node->m_node->m_set1l];
							for(idx=0;idx<b_node->m_node->m_set1l;idx++) set1_copy[idx]=b_node->m_node->m_set1[idx];
							set2_copy=new FeatureTerm *[b_node->m_node->m_set2l];
							for(idx=0;idx<b_node->m_node->m_set2l;idx++) set2_copy[idx]=b_node->m_node->m_set2[idx];

							stack.Insert(new SubsumptionStackNode(b_node->m_node->m_f1,b_node->m_node->m_f2,b_node->m_node->m_state,
																  b_node->m_node->m_feature_pos,
																  assignment_copy,set1_copy,b_node->m_node->m_set1l,set2_copy,b_node->m_node->m_set2l,b_node->m_node->m_assignment_pos));
						} else {
							stack.Insert(new SubsumptionStackNode(b_node->m_node->m_f1,b_node->m_node->m_f2,b_node->m_node->m_state,
																  b_node->m_node->m_feature_pos,
																  0,0,0,0,0,-1));
						} /* if */ 


						// bindings:
						while(bindings_a.Length()>b_node->n_bindings) {
							bindings_a.ExtractIni();
							bindings_b.ExtractIni();
						} // while 
						
						delete b_node;
					} else {
						SubsumptionStackNode *s_node;
						while(!stack.EmptyP()) {
							s_node=stack.ExtractIni();
							if (s_node->m_assignment!=0) {
								delete []s_node->m_assignment;
								s_node->m_set1l=0;
								s_node->m_set2l=0;
								delete []s_node->m_set1;
								delete []s_node->m_set2;
							} //  if  
							delete s_node;
						} /* while */ 
						res=false;
					} /* if */ 
				} else {
					SubsumptionStackNode *s_node;
					while(!stack.EmptyP()) {
						s_node=stack.ExtractIni();
						if (s_node->m_assignment!=0) {
							delete []s_node->m_assignment;
							s_node->m_set1l=0;
							s_node->m_set2l=0;
							delete []s_node->m_set1;
							delete []s_node->m_set2;
						} //  if  
						delete s_node;
					} /* while */ 
					res=false;
				} /* if */ 
			} /* if */ 

//			if (state==2) printf("Ok\n");
		} /* while */ 
	}

//	printf("*---- End Subsumption: %s ----*\n",(res ? "true":"false"));

	while(!bindings_a.EmptyP()) bindings_a.ExtractIni();
	while(!bindings_b.EmptyP()) bindings_b.ExtractIni();

	return res;
} /* FeatureTerm::subsumes */ 



bool get_set_assignment(int l1,int l2,int *assignment,int failure_position)
{
	int i=l1-1,j;
	int start_pos=0;
	bool collision;

	if (failure_position>=0 && failure_position<=l1-1) {
		i=failure_position;
		start_pos=failure_position;
	} /* if */ 

//	printf("<%i!> ",failure_position);

	for(j=failure_position+1;j<l1;j++) assignment[j]=-1;
	do{
		do{
			assignment[i]++;
			collision=false;
			for(j=0;j<i;j++) {
				if (assignment[i]==assignment[j]) collision=true;
			} // for  
		}while(collision && assignment[i]<l2);
		if (assignment[i]<l2) {
			i++;
		} else {
			if (i<l1) assignment[i]=-1;
			i--;
		} // if  

		if (i==l1) {
/*
			printf("{%i,%i} ",l1,l2);
			for(i=0;i<l1;i++) printf("%i ",assignment[i]);
			printf("\n");
*/
			return true;
		} /* if */ 
	}while(i>=start_pos);

//	printf("fail \n");

	return false;
} /* get_set_assignment */ 

